i:Id, A:MsgA, M:System. @i: A  M  A  M(i) 

latex

Definitions	Unit, P  Q, P  Q, SQType(T), {T}, a = b, , b, Prop, b, A, False, @i: A, P  Q, M1  M2, if b t else f fi, , P  Q, P & Q, D1  D2, M(i), x:A. B(x), System, MsgA, t  T, Id
Lemmas	Id wf, msga wf, msystem wf, assert wf, not wf, bnot wf, bool wf, eq id wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, bool sq, eqtt to assert, bool cases, ma-empty wf, ifthenelse wf, ma-sub wf, ma-empty-sub